Problem:
 b(b(x1)) -> a(a(a(x1)))
 b(a(b(x1))) -> a(x1)
 b(a(a(x1))) -> b(a(b(x1)))

Proof:
 Complexity Transformation Processor:
  strict:
   b(b(x1)) -> a(a(a(x1)))
   b(a(b(x1))) -> a(x1)
   b(a(a(x1))) -> b(a(b(x1)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [a](x0) = x0,
     
     [b](x0) = x0 + 80
    orientation:
     b(b(x1)) = x1 + 160 >= x1 = a(a(a(x1)))
     
     b(a(b(x1))) = x1 + 160 >= x1 = a(x1)
     
     b(a(a(x1))) = x1 + 80 >= x1 + 160 = b(a(b(x1)))
    problem:
     strict:
      b(a(a(x1))) -> b(a(b(x1)))
     weak:
      b(b(x1)) -> a(a(a(x1)))
      b(a(b(x1))) -> a(x1)
    Arctic Interpretation Processor:
     dimension: 3
     interpretation:
                [1  -& -&]  
      [a](x0) = [-& -& 1 ]x0
                [-& 1  -&]  ,
      
                [0  -& 0 ]  
      [b](x0) = [-& -& 0 ]x0
                [3  0  3 ]  
     orientation:
                    [2  -& 2 ]      [1  -& 1 ]                
      b(a(a(x1))) = [-& -& 2 ]x1 >= [-& -& 1 ]x1 = b(a(b(x1)))
                    [5  2  5 ]      [4  1  4 ]                
      
                 [3 0 3]      [3  -& -&]                
      b(b(x1)) = [3 0 3]x1 >= [-& -& 3 ]x1 = a(a(a(x1)))
                 [6 3 6]      [-& 3  -&]                
      
                    [1  -& 1 ]      [1  -& -&]          
      b(a(b(x1))) = [-& -& 1 ]x1 >= [-& -& 1 ]x1 = a(x1)
                    [4  1  4 ]      [-& 1  -&]          
     problem:
      strict:
       
      weak:
       b(a(a(x1))) -> b(a(b(x1)))
       b(b(x1)) -> a(a(a(x1)))
       b(a(b(x1))) -> a(x1)
     Qed